Search for: All records

Termination checking is a classic static analysis, and, within this focus, there are type-based approaches that formalize termination analysis as type systems (i.e., so that all well-typed programs terminate). But there are situations where a stronger termination property (which we call strongly-bounded termination) must be determined and, accordingly, we explore this property via a variant of the simply-typed λ-calculus called the bounded-time λ-calculus (BTC). This paper presents the BTC and its semantics and metatheory through a Coq formalization. Important examples (e.g., hardware synthesis from functional languages and detection of covert timing channels) motivating strongly-bounded termination and BTC are described as well. 

Brain age (BA), distinct from chronological age (CA), can be estimated from MRIs to evaluate neuroanatomic aging in cognitively normal (CN) individuals. BA, however, is a cross-sectional measure that summarizes cumulative neuroanatomic aging since birth. Thus, it conveys poorly recent or contemporaneous aging trends, which can be better quantified by the (temporal) pace P of brain aging. Many approaches to map P, however, rely on quantifying DNA methylation in whole-blood cells, which the blood–brain barrier separates from neural brain cells. We introduce a three-dimensional convolutional neural network (3D-CNN) to estimate P noninvasively from longitudinal MRI. Our longitudinal model (LM) is trained on MRIs from 2,055 CN adults, validated in 1,304 CN adults, and further applied to an independent cohort of 104 CN adults and 140 patients with Alzheimer’s disease (AD). In its test set, the LM computes P with a mean absolute error (MAE) of 0.16 y (7% mean error). This significantly outperforms the most accurate cross-sectional model, whose MAE of 1.85 y has 83% error. By synergizing the LM with an interpretable CNN saliency approach, we map anatomic variations in regional brain aging rates that differ according to sex, decade of life, and neurocognitive status. LM estimates of P are significantly associated with changes in cognitive functioning across domains. This underscores the LM’s ability to estimate P in a way that captures the relationship between neuroanatomic and neurocognitive aging. This research complements existing strategies for AD risk assessment that estimate individuals’ rates of adverse cognitive change with age.